/******************************************************************************
 * Top contributors (to current version):
 *   Mudathir Mohamed
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * set reduction.
 */

#ifndef CVC5__THEORY__SETS__SET_REDUCTION_H
#define CVC5__THEORY__SETS__SET_REDUCTION_H

#include <vector>

#include "cvc5_private.h"
#include "smt/env_obj.h"

namespace cvc5::internal {
namespace theory {
namespace sets {

/**
 * class for set reductions
 */
class SetReduction
{
 public:
  SetReduction();
  ~SetReduction();

  /**
   * @param node a term of the form (set.fold f t A) where
   *        f: (-> T1 T2 T2) is a binary operation
   *        t: T2 is the initial value
   *        A: (Set T1) is a set
   * @param asserts a list of assertions generated by this reduction
   * @return the reduction term (combine n) with asserts:
   * - (forall ((i Int))
   *    (let ((iMinusOne (- i 1)))
   *      (let ((uf_i (uf i)))
   *        (=>
   *          (and (>= i 1) (<= i n))
   *          (and
   *            (= (combine i) (f uf_i (combine iMinusOne)))
   *            (=
   *              (unionFn i)
   *              (set.union
   *                (set.singleton uf_i)
   *                (unionFn iMinusOne))))))))
   * - (= (combine 0) t)
   * - (= (unionFn 0) (as set.empty (Set T1)))
   * - (= A (unionFn n))
   * - (>= n 0))
   * where
   * n: Int is the cardinality of set A
   * uf:Int -> T1 is an uninterpreted function that represents elements of A
   * combine: Int -> T2 is an uninterpreted function
   * unionFn: Int -> (Set T1) is an uninterpreted function
   */
  static Node reduceFoldOperator(Node node, std::vector<Node>& asserts);

  /**
   * @param node of the form ((_ rel.aggr n1 ... nk) f initial A))
   * @return reduction term that uses map, fold, and group operators
   * as follows:
   * (set.map
   *   (lambda ((B Table)) (set.fold f initial B))
   *   ((_ rel.group n1 ... nk) A))
   */
  static Node reduceAggregateOperator(Node node);
  /**
   * @param n has the form ((rel.project n1 ... nk) A) where A has type (Set T)
   * @return (set.map (lambda ((t T)) ((_ tuple.project n1 ... nk) t)) A)
   */
  static Node reduceProjectOperator(Node n);
};

}  // namespace sets
}  // namespace theory
}  // namespace cvc5::internal

#endif /* CVC5__THEORY__SETS__SET_REDUCTION_H */
